p:FinProbSpace, n:, k:, X:({0..k}({0..n}Outcome)).
E(n;s.imax-list(map(i.X(i,s);upto(k))))  0  i < k
E(n;X(i)) 

latex

Definitions

x:A. B(x), t  T, {i..j}, RandomVariable(p;n), Top, i  j < k, P & Q, x. t(x), X  Y, xL. P(x), , P  Q, x:A. B(x), P  Q, P  Q, T, True, , S  T, suptype(S; T), , x(s), {T}, Outcome

Lemmas

int seg wf, p-outcome wf, nat wf, nat plus wf, finite-prob-space wf, expectation-monotone, imax-list wf, map wf, upto wf, nat plus inc, length-map, le wf, length upto, int inc rationals, qsum wf, int-rational, qsum-int, qle-int, imax-list-lb, l member wf, all functionality wrt iff, implies functionality wrt iff, member map, summand-qle-sum, non neg length, map length, qle wf, squash wf, true wf, rationals wf, expectation wf, subtype rel function, expectation-qsum